| Definitions | t  T,  x:A. B(x), es-val(es; e), x:A  B(x),  b, event_system{i:l}, atom{$n:n}, Id, fpf(A; a.B(a)), left + right, Knd, Type, x:A  B(x), es-dtype(es; i; x; T), s = t, t.1, es-E(es), es-vartype(es; i; x), top, fpf-cap(f; eq; x; z), P  Q, P   Q,   x. t(x), decl-state(ds), es-state(es; i), es-state-when(es; e), void, es-valtype(es; e), f(a), EState(T), rationals, pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>,  A, constant_function(f; A; B), kindcase(k; a.f(a); l,t.g(l;t)),  , e < e', qle(r; s), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  , Unit, Msg(M), type List, IdLnk, EOrderAxioms(E;pred?;info), EqDecider(T), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , es-after(es; x; e), id-deq, x.A(x), A c B, prop{i:l}, {x:A| B(x)} , let x,y = A in B(x;y), alle-at(es; i; e.P(e)), es-kindtype(es; i; k), effect-p(es; i; ds; k; T; x; f), decl-type{i:l}(ds; x) |
f:(decl-state(ds)